strong-subtype(A; B)
== subtype_rel(A; B)
== c subtype_rel({b:B| a:A. (b = a)} ; A)
== c (a1,a2:A. (a1 = a2)  (a1 = a2)) 

latex

---

clarification:

strong-subtype(A; B)
== subtype_rel(A; B)
== c subtype_rel({b:B| a:A. (b = a  B)} ; A)
== c (a1:A, a2:A. (a1 = a2  B)  (a1 = a2  A)) 

latex

Definitions	A c B, {x:A| B(x)} , x:A. B(x), x:A. B(x), P  Q, s = t
FDL editor aliases	strong-subtype